natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In first-order logic, the universal quantifier “” is the quantifier used to express — given a predicate with a free variable of type — the proposition denoted
which is meant to be true if and only if holds true for ALL possible elements of (all terms of type ) — whence the notation “A” (even if upside-down) for this quantifier.
This notion is “dual” (in fact adjoint, see below) to the existential quantifier “” which asserts that holds true for some .
But beware that is quite possible that may be provable (in a given context) for every term of type that can actually be constructed in that context, and yet cannot be proved: The proper internal definition of universal quantification is as a right adjoint to context extension as brought out by the definition (1) below and expanded on further below.
We work in a logic in which we are concerned with which propositions entail which other propositions (in a given context); in particular, two propositions which entail each other are considered logically equivalent, denoted by “”.
Let
be an arbitrary context,
a dependent type in ,
so that
We assume that we have a weakening rule that allows us to interpret any proposition in as
Then for
its universal quantification is any proposition in such that, given any proposition in , we have:
It is then a theorem that universal quantification of , if it exists, is unique. The existence is typically asserted as an axiom in a particular logic, but this may be also be deduced from other principles (as in the topos-theoretic discussion below).
Often one makes the appearance of the free variable in explicit by thinking of as a propositional function and writing instead. Then the rule appears as follows:
In terms of semantics (as for example topos-theoretic semantics; see below), the context extension from to corresponds to pulling back along a product projection , where is the interpretation of the type , and is the interpretation of . In other words, if a statement read in context is interpreted as a subobject of , then the statement read in context is interpreted by pulling back along the projection, obtaining a subobject of .
As observed by Lawvere, we are not particularly constrained to product projections; we can pull back along any map . (Often we have a class of display maps and require to be one of these.) Alternatively, any pullback functor can be construed as pulling back along an object , i.e., along the unique map corresponding to an object in the slice , since we have the identification .
In natural deduction the inference rules for the universal quantifier are given as
In set theory, recall that a predicate on a set in the internal logic of set theory is represented by the preimage of an injection . Because is an injection, each preimage is a subsingleton for all , which represents the internal propositions of the set theory. The internal universal quantifier is represented by the Cartesian product of the family of sets :
In terms of the internal logic in some ambient topos ,
the predicate is a (-1)-truncated object of the over-topos ;
a truth value is a (-1)-truncated object of itself.
Universal quantification is essentially the restriction of the direct image right adjoint of a canonical étale geometric morphism ,
where is the functor that takes an object to the product projection , where is the dependent sum (i.e., forgetful functor taking to ) that is left adjoint to , and where is the dependent product operation that is right adjoint to .
The dependent product operation restricts to propositions by pre- and postcomposition with the truncation adjunctions
to give universal quantification over the domain (or context) :
Dually, the extra left adjoint , obtained from the dependent sum by pre- and post-composition with the truncation adjunctions, expresses the existential quantifier. (The situation with the universal quantifier is somewhat simpler than for the existential one, since the dependent product automatically preserves -truncated objects (= subterminal objects), whereas the dependent sum does not.)
The same makes sense, verbatim, also in the (∞,1)-logic of any (∞,1)-topos.
This interpretation of universal quantification as the right adjoint to context extension is also used in the notion of hyperdoctrine.
In dependent type theory, the universal quantifier is the propositional truncation of the dependent product type of a family of h-propositions:
The axiom of function extensionality or weak function extensionality implies that the dependent product type of a family of h-propositions is always an h-proposition.
One doesn’t need all dependent product types to define universal quantifiers. The isProp types are definable without all dependent product types, by use of center of contraction, which are also definable without all dependent product types.
Formation rules for the universal quantifier:
Introduction rules for the universal quantifier:
Elimination rules for the universal quantifier:
Computation rules for the universal quantifier:
Uniqueness rules for the universal quantifier:
Closure of universal quantifiers under h-propositions rule:
This means that one could define the type-theoretic internal logic of a Heyting category or Boolean category which are not locally cartesian closed, for strongly predicative mathematics.
Let Set, let be the set of natural numbers and let be the subset of even natural numbers. This expresses the proposition .
Then the dependent product
is the set of sections of the bundle . But since over odd numbers the fiber of this bundle is the empty set, there is no possible value of such a section and hence the set of sections is itself the empty set, so the statement “all natural numbers are even” is, indeed, false.
The observation that substitution forms an adjoint pair/adjoint triple with the existential/universal quantifiers is due to
William Lawvere, Adjointness in Foundations, (tac:16), Dialectica 23 (1969), 281-296
William Lawvere, Quantifiers and sheaves, Actes, Congrès intern, math., 1970. Tome 1, p. 329 à 334 (pdf)
and further developed in
comprehension schema as an adjoint functor_, Proceedings of the AMS Symposium on Pure Mathematics XVII (1970), 1-14.
Last revised on November 13, 2023 at 13:48:39. See the history of this page for a list of all contributions to it.